Nuprl Lemma : ring_divs_wf
13,42
postcript
pdf
r
:RngSig,
p
,
q
:|
r
|.
p
|
q
in
r
latex
Up
rings
1
Definitions of Statement
a
|
b
in
r
Definitions
x
f
y
,
x
:
A
.
B
(
x
)
,
a
|
b
in
r
,
,
t
T
,
x
:
A
.
B
(
x
)
Lemmas
rng
sig
wf
,
rng
times
wf
,
rng
car
wf
origin
r:RngSig, p, q:|r|. p | q in r 
r:RngSig, p, q:|r|. p | q in r 
x:A. B(x) Tx:A. B(x)